ds:fpf(Id; x.Type{i}), da:fpf(Knd; k.Type{i}), P:(ecl(ds; da)prop{i':l}).
(k:Knd, test:(decl-state(ds)ma-valtype(da; k)). P(eclbase(k; test)))
 (a,b:ecl(ds; da). P(a)  P(b)  P(eclseq(a; b)))
 (a,b:ecl(ds; da). P(a)  P(b)  P(ecland(a; b)))
 (a,b:ecl(ds; da). P(a)  P(b)  P(eclor(a; b)))
 (a:ecl(ds; da). P(a)  P(eclrepeat(a)))
 (a:ecl(ds; da), n:. P(a)  P(eclact(a; n)))
 (a:ecl(ds; da), n:. P(a)  P(eclthrow(a; n)))
 (a:ecl(ds; da), l:( List). P(a)  P(eclcatch(a; l)))
 guard((x:ecl(ds; da). P(x))) 

latex

Definitions	x:A. B(x), prop{i:l}, P  Q, x(s), guard(T), t  T, x. t(x), ecl(ds; da), eclbase(k; test), eclseq(a; b), ecland(a; b), eclor(a; b), eclrepeat(a), eclact(a; n), eclthrow(a; n), eclcatch(a; l)
Lemmas	decl-state wf, ma-valtype wf, bool wf, nat wf, ecl wf, eclcatch wf, eclthrow wf, eclact wf, eclrepeat wf, eclor wf, ecland wf, eclseq wf, Knd wf, eclbase wf, fpf wf, Id wf